signature IR_STRUCTS =
sig
  include ATOMS
  structure Types : TYPES2
end

signature IR =
sig
  include IR_STRUCTS

  type pos = int

  structure Binop :
  sig
    datatype t
      = Plus
      | Minus
      | Times
      | Divide
      | Modus
      | And
      | Or
      | Eq
      | Ne
      | Gt
      | Ge
      | Lt
      | Le

    val equals : t * t -> bool
    val toString : t -> string
  end

  structure Le :
  sig
    datatype exp
      = Expvoid
      | IntNum of Intl.t
      | True
      | False
      | Null
      | Lval of {lval : lval, ty : Types.t}
      | BinopExp of {left : exp, bop : Binop.t, right : exp, ty : Types.t, pos : pos}
      | NotExp of exp * pos
      | Result
      | Imply of exp * exp * pos
      | Iff of exp * exp * pos
      | Forall of Id.t * Types.t * exp * pos
      | Exists of Id.t * Types.t * exp * pos
      | Pi of lval list list * pos
      | N of lval list * pos
      | D of lval list * pos
      | Prev of lval * pos
      | LList of exp * pos
      | Tree of exp * pos
      | Pred of Id.t * exp * pos
      | Let of exp * exp * exp * pos

    and lval
      = Var of {id : Id.t, ty : Types.t, pos: pos}
      | Ptr of lval * lval * pos
      | Sharp of Types.t
      | Inarray of {lval : lval, exp : exp, length : Intl.t, ty : Types.t, pos : pos}
      | Instruct of {lval : lval, id : Id.t, offSet : Intl.t, pos : pos}
      | Instruct2 of lval * Id.t * Id.t * int
      | Upd of lval * exp * exp
      | Sel of lval * exp

    val equalsExp : exp * exp -> bool
    val equalsLval : lval * lval -> bool
    val expToString : exp -> string
    val lvalToString : lval -> string
  end

  structure Stm :
  sig
    structure Map : ORD_MAP
    
    datatype t
      = AsnExp of {lval : Le.lval, exp : Le.exp, ty : Types.t, pos : pos}
      | AsnAlloc of {lval : Le.lval, ty : Types.t, pos : pos}
      | AsnCall of {lval : Le.lval, fid : Id.t, ty : Types.t, exps : Le.exp list, pos : pos}
      | If of Le.exp * t list * t list * pos
      | While of {condition : Le.exp, invariant : Le.exp, body : t list, pos : pos}
      | Return of {exp : Le.exp, fty : Types.t, pos : pos}
      | Call of Id.t * (Le.exp list) * pos
      | Free of Le.exp * pos
      | Prop of Le.exp * pos

    val bogus : unit -> t
    val endWithReturn : t -> bool
    val endWithReturns : t list -> bool
    val numCalls : t list -> (Id.t * int) list
    val toString : t -> string
  end

  structure Structs :
  sig
    datatype t
      = T of {name : Id.t,
              fields : {id : Id.t, ty : Types.t} list,
              pos : pos}
              
    val bogus : unit -> t
    val equals : t * t -> bool
    val toString : t -> string
  end

  structure Function :
  sig
    datatype t
      = T of {name : Id.t,
              rettype : Types.t,
              args : {id : Id.t, ty : Types.t} list,
              locals : {id : Id.t, ty : Types.t} list,
              stm : Stm.t list,
              pre : Le.exp,
              post : Le.exp,
              pos : pos}
    
    val name : t -> Id.t
    val toString : t -> string
  end

  structure Program :
  sig
    datatype t
      = T of {structs : Structs.t list,
              gvars : {id : Id.t, ty : Types.t} list,
              funcs : Function.t list,
              pos : pos}

    val bogus : unit -> t
    val toString : t -> string
  end
end
